The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(O(1), O(n^3)).

(0) Obligation:

Runtime Complexity TRS:
The TRS R consists of the following rules:

r0(0(x1)) → 0(r0(x1))
r0(1(x1)) → 1(r0(x1))
r0(m(x1)) → m(r0(x1))
r1(0(x1)) → 0(r1(x1))
r1(1(x1)) → 1(r1(x1))
r1(m(x1)) → m(r1(x1))
r0(b(x1)) → qr(0(b(x1)))
r1(b(x1)) → qr(1(b(x1)))
0(qr(x1)) → qr(0(x1))
1(qr(x1)) → qr(1(x1))
m(qr(x1)) → ql(m(x1))
0(ql(x1)) → ql(0(x1))
1(ql(x1)) → ql(1(x1))
b(ql(0(x1))) → 0(b(r0(x1)))
b(ql(1(x1))) → 1(b(r1(x1)))

Rewrite Strategy: INNERMOST

(1) CpxTrsToCdtProof (BOTH BOUNDS(ID, ID) transformation)

Converted CpxTRS to CDT

(2) Obligation:

Complexity Dependency Tuples Problem
Rules:

r0(0(z0)) → 0(r0(z0))
r0(1(z0)) → 1(r0(z0))
r0(m(z0)) → m(r0(z0))
r0(b(z0)) → qr(0(b(z0)))
r1(0(z0)) → 0(r1(z0))
r1(1(z0)) → 1(r1(z0))
r1(m(z0)) → m(r1(z0))
r1(b(z0)) → qr(1(b(z0)))
0(qr(z0)) → qr(0(z0))
0(ql(z0)) → ql(0(z0))
1(qr(z0)) → qr(1(z0))
1(ql(z0)) → ql(1(z0))
m(qr(z0)) → ql(m(z0))
b(ql(0(z0))) → 0(b(r0(z0)))
b(ql(1(z0))) → 1(b(r1(z0)))

Tuples:

R0(0(z0)) → c(0'(r0(z0)), R0(z0))
R0(1(z0)) → c1(1'(r0(z0)), R0(z0))
R0(m(z0)) → c2(M(r0(z0)), R0(z0))
R0(b(z0)) → c3(0'(b(z0)), B(z0))
R1(0(z0)) → c4(0'(r1(z0)), R1(z0))
R1(1(z0)) → c5(1'(r1(z0)), R1(z0))
R1(m(z0)) → c6(M(r1(z0)), R1(z0))
R1(b(z0)) → c7(1'(b(z0)), B(z0))
0'(qr(z0)) → c8(0'(z0))
0'(ql(z0)) → c9(0'(z0))
1'(qr(z0)) → c10(1'(z0))
1'(ql(z0)) → c11(1'(z0))
M(qr(z0)) → c12(M(z0))
B(ql(0(z0))) → c13(0'(b(r0(z0))), B(r0(z0)), R0(z0))
B(ql(1(z0))) → c14(1'(b(r1(z0))), B(r1(z0)), R1(z0))

S tuples:

R0(0(z0)) → c(0'(r0(z0)), R0(z0))
R0(1(z0)) → c1(1'(r0(z0)), R0(z0))
R0(m(z0)) → c2(M(r0(z0)), R0(z0))
R0(b(z0)) → c3(0'(b(z0)), B(z0))
R1(0(z0)) → c4(0'(r1(z0)), R1(z0))
R1(1(z0)) → c5(1'(r1(z0)), R1(z0))
R1(m(z0)) → c6(M(r1(z0)), R1(z0))
R1(b(z0)) → c7(1'(b(z0)), B(z0))
0'(qr(z0)) → c8(0'(z0))
0'(ql(z0)) → c9(0'(z0))
1'(qr(z0)) → c10(1'(z0))
1'(ql(z0)) → c11(1'(z0))
M(qr(z0)) → c12(M(z0))
B(ql(0(z0))) → c13(0'(b(r0(z0))), B(r0(z0)), R0(z0))
B(ql(1(z0))) → c14(1'(b(r1(z0))), B(r1(z0)), R1(z0))

K tuples:none
Defined Rule Symbols:

r0, r1, 0, 1, m, b

Defined Pair Symbols:

R0, R1, 0', 1', M, B

Compound Symbols:

c, c1, c2, c3, c4, c5, c6, c7, c8, c9, c10, c11, c12, c13, c14

(3) CdtUnreachableProof (EQUIVALENT transformation)

The following tuples could be removed as they are not reachable from basic start terms:

R0(0(z0)) → c(0'(r0(z0)), R0(z0))
R0(1(z0)) → c1(1'(r0(z0)), R0(z0))
R0(m(z0)) → c2(M(r0(z0)), R0(z0))
R0(b(z0)) → c3(0'(b(z0)), B(z0))
R1(0(z0)) → c4(0'(r1(z0)), R1(z0))
R1(1(z0)) → c5(1'(r1(z0)), R1(z0))
R1(m(z0)) → c6(M(r1(z0)), R1(z0))
R1(b(z0)) → c7(1'(b(z0)), B(z0))
B(ql(0(z0))) → c13(0'(b(r0(z0))), B(r0(z0)), R0(z0))
B(ql(1(z0))) → c14(1'(b(r1(z0))), B(r1(z0)), R1(z0))

(4) Obligation:

Complexity Dependency Tuples Problem
Rules:

r0(0(z0)) → 0(r0(z0))
r0(1(z0)) → 1(r0(z0))
r0(m(z0)) → m(r0(z0))
r0(b(z0)) → qr(0(b(z0)))
r1(0(z0)) → 0(r1(z0))
r1(1(z0)) → 1(r1(z0))
r1(m(z0)) → m(r1(z0))
r1(b(z0)) → qr(1(b(z0)))
0(qr(z0)) → qr(0(z0))
0(ql(z0)) → ql(0(z0))
1(qr(z0)) → qr(1(z0))
1(ql(z0)) → ql(1(z0))
m(qr(z0)) → ql(m(z0))
b(ql(0(z0))) → 0(b(r0(z0)))
b(ql(1(z0))) → 1(b(r1(z0)))

Tuples:

0'(qr(z0)) → c8(0'(z0))
0'(ql(z0)) → c9(0'(z0))
1'(qr(z0)) → c10(1'(z0))
1'(ql(z0)) → c11(1'(z0))
M(qr(z0)) → c12(M(z0))

S tuples:

0'(qr(z0)) → c8(0'(z0))
0'(ql(z0)) → c9(0'(z0))
1'(qr(z0)) → c10(1'(z0))
1'(ql(z0)) → c11(1'(z0))
M(qr(z0)) → c12(M(z0))

K tuples:none
Defined Rule Symbols:

r0, r1, 0, 1, m, b

Defined Pair Symbols:

0', 1', M

Compound Symbols:

c8, c9, c10, c11, c12

(5) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

1'(qr(z0)) → c10(1'(z0))
1'(ql(z0)) → c11(1'(z0))

We considered the (Usable) Rules:none
And the Tuples:

0'(qr(z0)) → c8(0'(z0))
0'(ql(z0)) → c9(0'(z0))
1'(qr(z0)) → c10(1'(z0))
1'(ql(z0)) → c11(1'(z0))
M(qr(z0)) → c12(M(z0))

The order we found is given by the following interpretation:
Polynomial interpretation :

POL(0'(x₁)) = 0   
POL(1'(x₁)) = [4]x₁   
POL(M(x₁)) = [5]x₁   
POL(c10(x₁)) = x₁   
POL(c11(x₁)) = x₁   
POL(c12(x₁)) = x₁   
POL(c8(x₁)) = x₁   
POL(c9(x₁)) = x₁   
POL(ql(x₁)) = [4] + x₁   
POL(qr(x₁)) = [5] + x₁   

(6) Obligation:

Complexity Dependency Tuples Problem
Rules:

r0(0(z0)) → 0(r0(z0))
r0(1(z0)) → 1(r0(z0))
r0(m(z0)) → m(r0(z0))
r0(b(z0)) → qr(0(b(z0)))
r1(0(z0)) → 0(r1(z0))
r1(1(z0)) → 1(r1(z0))
r1(m(z0)) → m(r1(z0))
r1(b(z0)) → qr(1(b(z0)))
0(qr(z0)) → qr(0(z0))
0(ql(z0)) → ql(0(z0))
1(qr(z0)) → qr(1(z0))
1(ql(z0)) → ql(1(z0))
m(qr(z0)) → ql(m(z0))
b(ql(0(z0))) → 0(b(r0(z0)))
b(ql(1(z0))) → 1(b(r1(z0)))

Tuples:

0'(qr(z0)) → c8(0'(z0))
0'(ql(z0)) → c9(0'(z0))
1'(qr(z0)) → c10(1'(z0))
1'(ql(z0)) → c11(1'(z0))
M(qr(z0)) → c12(M(z0))

S tuples:

0'(qr(z0)) → c8(0'(z0))
0'(ql(z0)) → c9(0'(z0))
M(qr(z0)) → c12(M(z0))

K tuples:

1'(qr(z0)) → c10(1'(z0))
1'(ql(z0)) → c11(1'(z0))

Defined Rule Symbols:

r0, r1, 0, 1, m, b

Defined Pair Symbols:

0', 1', M

Compound Symbols:

c8, c9, c10, c11, c12

(7) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^2))) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

M(qr(z0)) → c12(M(z0))

We considered the (Usable) Rules:none
And the Tuples:

0'(qr(z0)) → c8(0'(z0))
0'(ql(z0)) → c9(0'(z0))
1'(qr(z0)) → c10(1'(z0))
1'(ql(z0)) → c11(1'(z0))
M(qr(z0)) → c12(M(z0))

The order we found is given by the following interpretation:
Polynomial interpretation :

POL(0'(x₁)) = 0   
POL(1'(x₁)) = 0   
POL(M(x₁)) = [2]x₁ + x₁²   
POL(c10(x₁)) = x₁   
POL(c11(x₁)) = x₁   
POL(c12(x₁)) = x₁   
POL(c8(x₁)) = x₁   
POL(c9(x₁)) = x₁   
POL(ql(x₁)) = 0   
POL(qr(x₁)) = [1] + x₁   

(8) Obligation:

Complexity Dependency Tuples Problem
Rules:

r0(0(z0)) → 0(r0(z0))
r0(1(z0)) → 1(r0(z0))
r0(m(z0)) → m(r0(z0))
r0(b(z0)) → qr(0(b(z0)))
r1(0(z0)) → 0(r1(z0))
r1(1(z0)) → 1(r1(z0))
r1(m(z0)) → m(r1(z0))
r1(b(z0)) → qr(1(b(z0)))
0(qr(z0)) → qr(0(z0))
0(ql(z0)) → ql(0(z0))
1(qr(z0)) → qr(1(z0))
1(ql(z0)) → ql(1(z0))
m(qr(z0)) → ql(m(z0))
b(ql(0(z0))) → 0(b(r0(z0)))
b(ql(1(z0))) → 1(b(r1(z0)))

Tuples:

0'(qr(z0)) → c8(0'(z0))
0'(ql(z0)) → c9(0'(z0))
1'(qr(z0)) → c10(1'(z0))
1'(ql(z0)) → c11(1'(z0))
M(qr(z0)) → c12(M(z0))

S tuples:

0'(qr(z0)) → c8(0'(z0))
0'(ql(z0)) → c9(0'(z0))

K tuples:

1'(qr(z0)) → c10(1'(z0))
1'(ql(z0)) → c11(1'(z0))
M(qr(z0)) → c12(M(z0))

Defined Rule Symbols:

r0, r1, 0, 1, m, b

Defined Pair Symbols:

0', 1', M

Compound Symbols:

c8, c9, c10, c11, c12

(9) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^3))) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

0'(ql(z0)) → c9(0'(z0))

We considered the (Usable) Rules:none
And the Tuples:

0'(qr(z0)) → c8(0'(z0))
0'(ql(z0)) → c9(0'(z0))
1'(qr(z0)) → c10(1'(z0))
1'(ql(z0)) → c11(1'(z0))
M(qr(z0)) → c12(M(z0))

The order we found is given by the following interpretation:
Polynomial interpretation :

POL(0'(x₁)) = x₁²   
POL(1'(x₁)) = 0   
POL(M(x₁)) = 0   
POL(c10(x₁)) = x₁   
POL(c11(x₁)) = x₁   
POL(c12(x₁)) = x₁   
POL(c8(x₁)) = x₁   
POL(c9(x₁)) = x₁   
POL(ql(x₁)) = [1] + x₁   
POL(qr(x₁)) = x₁   

(10) Obligation:

Complexity Dependency Tuples Problem
Rules:

r0(0(z0)) → 0(r0(z0))
r0(1(z0)) → 1(r0(z0))
r0(m(z0)) → m(r0(z0))
r0(b(z0)) → qr(0(b(z0)))
r1(0(z0)) → 0(r1(z0))
r1(1(z0)) → 1(r1(z0))
r1(m(z0)) → m(r1(z0))
r1(b(z0)) → qr(1(b(z0)))
0(qr(z0)) → qr(0(z0))
0(ql(z0)) → ql(0(z0))
1(qr(z0)) → qr(1(z0))
1(ql(z0)) → ql(1(z0))
m(qr(z0)) → ql(m(z0))
b(ql(0(z0))) → 0(b(r0(z0)))
b(ql(1(z0))) → 1(b(r1(z0)))

Tuples:

0'(qr(z0)) → c8(0'(z0))
0'(ql(z0)) → c9(0'(z0))
1'(qr(z0)) → c10(1'(z0))
1'(ql(z0)) → c11(1'(z0))
M(qr(z0)) → c12(M(z0))

S tuples:

0'(qr(z0)) → c8(0'(z0))

K tuples:

1'(qr(z0)) → c10(1'(z0))
1'(ql(z0)) → c11(1'(z0))
M(qr(z0)) → c12(M(z0))
0'(ql(z0)) → c9(0'(z0))

Defined Rule Symbols:

r0, r1, 0, 1, m, b

Defined Pair Symbols:

0', 1', M

Compound Symbols:

c8, c9, c10, c11, c12

(11) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

0'(qr(z0)) → c8(0'(z0))

We considered the (Usable) Rules:none
And the Tuples:

0'(qr(z0)) → c8(0'(z0))
0'(ql(z0)) → c9(0'(z0))
1'(qr(z0)) → c10(1'(z0))
1'(ql(z0)) → c11(1'(z0))
M(qr(z0)) → c12(M(z0))

The order we found is given by the following interpretation:
Polynomial interpretation :

POL(0'(x₁)) = x₁   
POL(1'(x₁)) = 0   
POL(M(x₁)) = x₁   
POL(c10(x₁)) = x₁   
POL(c11(x₁)) = x₁   
POL(c12(x₁)) = x₁   
POL(c8(x₁)) = x₁   
POL(c9(x₁)) = x₁   
POL(ql(x₁)) = x₁   
POL(qr(x₁)) = [1] + x₁   

(12) Obligation:

Complexity Dependency Tuples Problem
Rules:

r0(0(z0)) → 0(r0(z0))
r0(1(z0)) → 1(r0(z0))
r0(m(z0)) → m(r0(z0))
r0(b(z0)) → qr(0(b(z0)))
r1(0(z0)) → 0(r1(z0))
r1(1(z0)) → 1(r1(z0))
r1(m(z0)) → m(r1(z0))
r1(b(z0)) → qr(1(b(z0)))
0(qr(z0)) → qr(0(z0))
0(ql(z0)) → ql(0(z0))
1(qr(z0)) → qr(1(z0))
1(ql(z0)) → ql(1(z0))
m(qr(z0)) → ql(m(z0))
b(ql(0(z0))) → 0(b(r0(z0)))
b(ql(1(z0))) → 1(b(r1(z0)))

Tuples:

0'(qr(z0)) → c8(0'(z0))
0'(ql(z0)) → c9(0'(z0))
1'(qr(z0)) → c10(1'(z0))
1'(ql(z0)) → c11(1'(z0))
M(qr(z0)) → c12(M(z0))

S tuples:none
K tuples:

1'(qr(z0)) → c10(1'(z0))
1'(ql(z0)) → c11(1'(z0))
M(qr(z0)) → c12(M(z0))
0'(ql(z0)) → c9(0'(z0))
0'(qr(z0)) → c8(0'(z0))

Defined Rule Symbols:

r0, r1, 0, 1, m, b

Defined Pair Symbols:

0', 1', M

Compound Symbols:

c8, c9, c10, c11, c12

(13) SIsEmptyProof (EQUIVALENT transformation)

The set S is empty

(14) BOUNDS(O(1), O(1))